p:FinProbSpace, n:, X, Y:RandomVariable(p;n). E(n;X + Y) = (E(n;X) + E(n;Y))   

latex

Definitions	#$n, , FinProbSpace, RandomVariable(p;n), X + Y, q*X, r + s, T, , {x:A| B(x)} , , A  B, A, False, <a, b>, r * s, True, P  Q, x:A  B(x), s = t, P & Q, P  Q, P  Q, x:AB(x), , E(n;F), x:A. B(x), t  T, x.A(x), f(a), {i..j}, ||as||, b
Lemmas	length wf1, int seg wf, qmul wf, expectation wf, rationals wf, qmul one qrng, true wf, squash wf, qadd wf, finite-prob-space wf, nat wf, random-variable wf, int inc rationals, expectation-linear